Nuprl Lemma : do-apply-p-lift 11,40
A, B:Type, P:(A), d:(x:ADec(P(x))), f:({x:A| P(x)} B), x:A.
(can-apply(p-lift(d;f);x))  (do-apply(p-lift(d;f);x) = f(x)) 
latex

ProofTree

Definitionsb, do-apply(f;x), p-lift(d;f), can-apply(f;x), x:AB(x), P  Q, Type, t  T, s = t, , f(a), x(s), Dec(P), x:A. B(x), {x:A| B(x)} , Void, x:A.B(x), Top, S  T, suptype(S; T), x.A(x), x. t(x), False, A, inr x , outl(x), True, inl x , left + right, P  Q
Lemmastrue wf, false wf, assert wf, can-apply wf, p-lift wf, top wf, member wf, decidable wf

origin